<html>
<head><meta charset="utf-8"><title>not-logic · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html">not-logic</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="204632339"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204632339" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> pksunkara <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204632339">(Jul 22 2020 at 05:48)</a>:</h4>
<p>I am not sure if this has been already discussed or not, but I have been thinking about this for a long time and with all the work on Chalk, I think this is possible now.</p>
<div class="codehilite"><pre><span></span><code><span class="k">pub</span><span class="w"> </span><span class="k">trait</span><span class="w"> </span><span class="n">A</span><span class="p">;</span><span class="w"></span>
<span class="k">pub</span><span class="w"> </span><span class="k">trait</span><span class="w"> </span><span class="n">B</span><span class="p">;</span><span class="w"></span>

<span class="k">pub</span><span class="w"> </span><span class="k">struct</span> <span class="nc">Z</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"></span>
<span class="k">where</span><span class="w"> </span><span class="n">T</span>: <span class="nc">A</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="o">!</span><span class="n">B</span><span class="w"></span>
</code></pre></div>



<a name="204632353"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204632353" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> pksunkara <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204632353">(Jul 22 2020 at 05:48)</a>:</h4>
<p>And also other logics in the where condition</p>



<a name="204695636"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204695636" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bram van den Heuvel <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204695636">(Jul 22 2020 at 17:19)</a>:</h4>
<p>I believe this has been discussed before, this might be useful: <a href="https://github.com/rust-lang/rust/issues/42721">https://github.com/rust-lang/rust/issues/42721</a></p>



<a name="204810891"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204810891" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> pksunkara <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204810891">(Jul 23 2020 at 15:15)</a>:</h4>
<p>Yup, I read that one. That's where I realized that it's not supported. Specialization doesn't help some use cases too. I think the next steps if we want to have something like this is to add it in chalk. I am just asking the contributors opinions here. cc <span class="user-mention" data-user-id="232957">@Jack Huey</span> <span class="user-mention" data-user-id="116009">@nikomatsakis</span></p>



<a name="204824077"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204824077" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204824077">(Jul 23 2020 at 16:58)</a>:</h4>
<p><span class="user-mention" data-user-id="254853">@pksunkara</span> are you asking is this possible in Chalk or rustc?</p>



<a name="204824187"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204824187" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204824187">(Jul 23 2020 at 16:59)</a>:</h4>
<p>So, in Chalk</p>



<a name="204824210"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204824210" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204824210">(Jul 23 2020 at 16:59)</a>:</h4>
<p>this I think would heavily rely on negative goals</p>



<a name="204824222"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204824222" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204824222">(Jul 23 2020 at 16:59)</a>:</h4>
<p>and then runs the risk of negative cycles</p>



<a name="204824262"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204824262" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204824262">(Jul 23 2020 at 16:59)</a>:</h4>
<p>which we currently don't handle in slg</p>



<a name="204824322"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204824322" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204824322">(Jul 23 2020 at 17:00)</a>:</h4>
<p>and recursive solver is in limbo</p>



<a name="204826228"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204826228" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> pksunkara <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204826228">(Jul 23 2020 at 17:16)</a>:</h4>
<p>For it to be implemented in rustc it would need to be implemented in chalk first since we are aiming for chalk to be the main trait solver in rustc</p>



<a name="204826248"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204826248" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> pksunkara <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204826248">(Jul 23 2020 at 17:16)</a>:</h4>
<p>So yeah I was asking about the possibility of this in chalk first</p>



<a name="204827562"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/204827562" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#204827562">(Jul 23 2020 at 17:29)</a>:</h4>
<p>Yeah, honestly this is more of t-lang/RFC territory. There is a question of whether or not this <em>could</em> be implemented in Chalk and/or what it would take. But the bigger question is whether this would be or should be part of the rust lang</p>



<a name="205626580"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205626580" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205626580">(Jul 31 2020 at 18:43)</a>:</h4>
<p>The real question is what <code>!</code> means</p>



<a name="205626740"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205626740" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205626740">(Jul 31 2020 at 18:44)</a>:</h4>
<p>In particular, if <code>T: !Foo</code> means "there isn't currently an impl of <code>Foo</code> for <code>T</code>", I see that as a non-starter, both because it means we'd have general purpose negative goals and in particular cyclic goals, and because of semver</p>



<a name="205626764"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205626764" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205626764">(Jul 31 2020 at 18:44)</a>:</h4>
<p>But there's an alternative world where people can write negative impls</p>



<a name="205626780"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205626780" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205626780">(Jul 31 2020 at 18:44)</a>:</h4>
<p>And in that case <code>T: !Foo</code> means <em>there is an explicit negative impl</em></p>



<a name="205626818"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205626818" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205626818">(Jul 31 2020 at 18:45)</a>:</h4>
<p>And coherence has the job of proving that all positive and negative impls are disjoint</p>



<a name="205626835"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205626835" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205626835">(Jul 31 2020 at 18:45)</a>:</h4>
<p>That I think works reasonably well</p>



<a name="205626893"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205626893" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205626893">(Jul 31 2020 at 18:45)</a>:</h4>
<p>and it means that "negative goals" in Rust's surface syntax are actually <em>positive goals</em> in the desugaring (a positive goal proving <code>!Foo</code>)</p>



<a name="205629759"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205629759" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205629759">(Jul 31 2020 at 19:10)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/144729-wg-traits/topic/not-logic/near/205626780">said</a>:</p>
<blockquote>
<p>And in that case <code>T: !Foo</code> means <em>there is an explicit negative impl</em></p>
</blockquote>
<p>I don't quite understand how this is different than the previous</p>



<a name="205629784"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205629784" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205629784">(Jul 31 2020 at 19:11)</a>:</h4>
<p>Or I guess, I don't understand how <em>this</em> doesn't have problems with cyclic and semver</p>



<a name="205637454"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205637454" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205637454">(Jul 31 2020 at 20:21)</a>:</h4>
<p>the idea is that we would NOT translate a predicate like <code>T: !Foo</code> into <code>not { Implemented(T: Foo) }</code></p>



<a name="205637471"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205637471" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205637471">(Jul 31 2020 at 20:21)</a>:</h4>
<p>but rather into <code>NotImplemented(T: Foo)</code></p>



<a name="205637477"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205637477" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205637477">(Jul 31 2020 at 20:21)</a>:</h4>
<p>and then if you have a <code>impl !Foo for u32</code></p>



<a name="205637487"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205637487" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205637487">(Jul 31 2020 at 20:21)</a>:</h4>
<p>that would generate a program clause like <code>NotImplemented(u32: Foo)</code></p>



<a name="205637544"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205637544" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205637544">(Jul 31 2020 at 20:22)</a>:</h4>
<p>but if you don't have such an impl, say for <code>i32</code>, then <code>i32: !Foo</code> is not provable</p>



<a name="205637605"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205637605" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205637605">(Jul 31 2020 at 20:23)</a>:</h4>
<p>so the <code>!</code> syntax in Rust would not correspond to <code>not { G }</code> goals in chalk</p>



<a name="205637863"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205637863" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205637863">(Jul 31 2020 at 20:25)</a>:</h4>
<p>would this basically be like a <code>NotFoo</code> trait whose only connection to <code>Foo</code> is through coherence?</p>



<a name="205638023"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/not-logic/near/205638023" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/not-logic.html#205638023">(Jul 31 2020 at 20:26)</a>:</h4>
<p>yes</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>